Inference at * 1 1 4 
Iof proof for Lemma absval eq:



1. x : 
2. y : 
3. x < 0
4. y < 0
  ((-x) = (-y))  x =  y 

latex

 by ((((((Unfold `pm_equal` 0) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n
C),(first_nat 3:n)) (first_tok SupInf:t) inil_term)))) 
CollapseTHEN (Try (D (-1))))) 

CoCollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 1000:n)) (first_tok :t
C) inil_term))) 

latex

C.

Definitions

, t  T, P  Q, P  Q, P & Q, P  Q, i =  j, P  Q